Nuprl Lemma : ma-pre_wf
11,40
postcript
pdf
M
:MsgA,
a
:Id,
s
:
M
.state.
M
.pre(
a
,
s
)
latex
Definitions
Id
,
t
T
,
x
:
A
.
B
(
x
)
,
State(
ds
)
,
,
Type
,
x
:
A
B
(
x
)
,
x
.
A
(
x
)
,
x
.
t
(
x
)
,
a
:
A
fp
B
(
a
)
,
Top
,
P
Q
,
f
(
x
)
,
f
(
a
)
,
b
,
IdDeq
,
x
dom(
f
)
,
,
z
!=
f
(
x
)
P
(
a
;
z
)
,
M
.pre(
a
,
s
)
,
M
.state
,
x
:
A
B
(
x
)
,
MsgA
Lemmas
msga
wf
,
fpf-dom
wf
,
id-deq
wf
,
assert
wf
,
fpf-ap
wf
,
fpf-trivial-subtype-top
,
bool
wf
,
ma-state
wf
,
Id
wf
origin
M:MsgA, a:Id, s:M.state. M.pre(a,s) 
M:MsgA, a:Id, s:M.state. M.pre(a,s) Tx:A. B(x)
B(x)
x.A(x)
x. t(x) B(a)
Q
b dom(f) P(a;z)
B(x)